Basically looking at tree replacements of a certain type
Basically looking at tree replacements of a certain type
Enumerating Possible Axiom Systems
Enumerating Possible Axiom Systems
First, consider cases where we have identified the operators [we can also consider cases where we’ve identified constants (i.e. arity-0 operators) ]
Single binary operator
Single binary operator
With pure substitution, and initial conditions that are self application onto the axiom, do we generate exactly the “true” theorems here:
In[]:=
#<->a_&/@Groupings[{a_,b_,b_},CenterDot->2]
Out[]=
{(a_·b_)·b_a_,a_·(b_·b_)a_}
In[]:=
ResourceFunction["TokenEventGraph"][{{u_,v_}:>Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]]},{#},2,"TokenLabeling"->False,"TokenMultiplicity"->Automatic,AspectRatio->1]&/@(#<->a_&/@Groupings[{a_,b_,b_},CenterDot->2])
Out[]=
,
In[]:=
(Cases[VertexList[#],_TwoWayRule]/.p_Pattern:>First[p])&/@%
In[]:=
ResourceFunction["TokenEventGraph"][{{u_,v_}:>Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]]},{#},1,"TokenLabeling"->True,"TokenMultiplicity"->Automatic,AspectRatio->1]&/@(#<->a_&/@Groupings[{a_,b_,b_},CenterDot->2])
Out[]=
,
In[]:=
findTree[patt_TwoWayRule]:=(UndirectedGraph[TreeGraph[ExpressionTree[#,TreeElementLabel->(All->None),TreeElementStyle->(All->Tiny)]],ImageSize->Tiny]&/@(patt/.p_Pattern:>First[p]))
[[[ Tree rendering : ]]]
[[[ Tree rendering : ]]]
In[]:=
TWPTreeGraph[patt_TwoWayRule,opts___]:=With[{g=TreeGraph[ExpressionTree[(#)]],vars=Union[Level[#,{-1}]]},Graph[treeLayout[EdgeList[g]],opts,VertexStyle->(#->If[MemberQ[vars,First[#]],ColorData[10][First@FirstPosition[vars,First[#]]],Gray]&/@VertexList[g])]]&/@(patt/.p_Pattern:>First[p])
In[]:=
treeLayout[g_]:=Graph[g,VertexCoordinates->Thread[VertexList@g->GraphEmbedding@GraphTree@g]]
In[]:=
%518[[1,11]]
In[]:=
UndirectedGraph[TreeGraph[ExpressionTree[#,TreeElementLabel->(All->None),TreeElementStyle->(All->Tiny)]]]&/@(((((((a·b)·b)·c)·d)·d)·e)·ef)
Out[]=
In[]:=
(Map[findTree,Cases[VertexList[#],_TwoWayRule]&@ResourceFunction["TokenEventGraph"][{{u_,v_}:>Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]]},{#},1,"TokenLabeling"->False,"TokenMultiplicity"->Automatic,AspectRatio->1]]&)/@(#<->a_&/@Groupings[{a_,b_,b_},CenterDot->2])
Out[]=
,
,
,
,
,
,
,
,
,
,
,
,
,
The a, b etc. should be shown as different colors of leaves
Even tinier axiom systems:
Even tinier axiom systems:
Enumeration of possible axiom systems
Enumeration of possible axiom systems
These are all identical because the “a” must be inserted in the same number of places on the LHS:
Are there clusters of nodes here that would be “named the same theorem”
Interpretation
Interpretation
Spacelike separated tokens can coexist in a particular branch of mathematical history
Spacelike separated tokens can coexist in a particular branch of mathematical history
Entailment/derivation cone of a statement is everything that can be derived just from that statement
Entailment/derivation cone of a statement is everything that can be derived just from that statement
E.g. for Euclid we have plots of what gets entailed from each of the axioms
E.g. in group theory we can have entailments (i.e. statements) from the general group axioms ... then we’ll have more entailments if we add the specific relations of a group
“Point to point geodesic”: there is a single statement that leads to another statement
“Point to point geodesic”: there is a single statement that leads to another statement
Many proofs may take multiple “input points” (i.e. axioms) to derive a single statement
In ATP one normally adds in the potential theorem, and sees if one can derive a tautology [[[ this has to do with using completions to make the path finding simpler ]]]
Is there confluence in these TEGs?
Is there confluence in these TEGs?
What are the reference frames of mathematical development?
What are the reference frames of mathematical development?
These contain statements that are “instantaneously independent” (?)
How are statements laid out branchially in these slices?
How are statements laid out branchially in these slices?
When statements are far apart, this means that to derive one from the other will take awhile...
What does it look like when the theory is decidable?
What does it look like when the theory is decidable?
How do models (as in model theory) relate to all of this?
How do models (as in model theory) relate to all of this?
What does the presence of infinite paths mean? [Basically computational irreducibility]
What does the presence of infinite paths mean? [Basically computational irreducibility]
Notion of “truth”:
Notion of “truth”:
Find a statement that you think is “obviously true” e.g. a == a
Now look for all statements that are connected to this; these are the true statements
Now look for all statements that are connected to this; these are the true statements
[True as in a==a has an entailment cone]
[But if there are other “obviously true” statements, they could have their own entailment]
[But if there are other “obviously true” statements, they could have their own entailment]
Notion of falsity
Notion of falsity
This is harder to define. Perhaps a_ == b_
“Physicalized Interpretation”
“Physicalized Interpretation”
Proof structure knits together metamathematical space
Proof structure knits together metamathematical space
What is metamathematical energy? Metamathematical gravity?
What is metamathematical energy? Metamathematical gravity?
Density of activity in regions of metamathematical space
Singularity theorems if there is enough proof density, the theory will eventually be decidable
Singularity theorems if there is enough proof density, the theory will eventually be decidable
[ So presumably this means there are no more new theorems produced ]
Infinite future of math: expansion of the metamathematical universe, together with a bunch of black holes being formed
Infinite future of math: expansion of the metamathematical universe, together with a bunch of black holes being formed
Future entailment cone of the Peano axioms will still be infinite ... but there will be lots of “burned out” subcases left behind
Model Theory
Model Theory
If there is a model of · , then for every of the k choices of each variable, the LHS and RHS will be the same...
So any given statement has essentially a barcode of what values its two sides can take on......
The model defines equivalences between expressions.... Which means that in the proof graph there is an overlay for a given model that connects things equivalent in that model...
?? Finding a model is like a finding a valid foliation ??
?? Finding a model is like a finding a valid foliation ??
Actually more like find an “observer sampling”
You can get proof results that are equivalent to model results by adding enough relations
You can get proof results that are equivalent to model results by adding enough relations
Given a model, there is a definite representation for a==a ;
Given a model, there is a definite representation for a==a ;
... so all tautologies [under the model] can be “painted” by seeing whether they have the same “bar code” as a==a
... so all tautologies [under the model] can be “painted” by seeing whether they have the same “bar code” as a==a
Assume that from an axiom A one can derive a theorem S. A model will give a “barcode” for LHS[A] and LHS[S]. The fact that S can be derived from A .... what does it say about the bar codes ???
Assume that from an axiom A one can derive a theorem S. A model will give a “barcode” for LHS[A] and LHS[S]. The fact that S can be derived from A .... what does it say about the bar codes ???
Enumerating values of expressions for a particular model
Enumerating values of expressions for a particular model
So therefore the model is establishing a relation that cannot be derived proof theoretically.....
“Model values” are like hash codes: they are unequal, then the statements can’t follow from each other; but if they are equal, that might just be a “coincidence”/”hash collision” and have nothing to do getting from one to the other by a proof
“Model values” are like hash codes: they are unequal, then the statements can’t follow from each other; but if they are equal, that might just be a “coincidence”/”hash collision” and have nothing to do getting from one to the other by a proof
If the “model codes” are equal, one form of proof (e.g, substitution) might not connect them, but another (e.g. cosubstitution) might do it....